Journals
  Publication Years
  Keywords
Search within results Open Search
Please wait a minute...
For Selected: Toggle Thumbnails
Strategy of invalid clause elimination in first-order logic theorem prover
Shipan JIANG, Shuwei CHEN, Guoyan ZENG
Journal of Computer Applications    2024, 44 (3): 677-682.   DOI: 10.11772/j.issn.1001-9081.2023030284
Abstract164)   HTML16)    PDF (905KB)(115)       Save

In the first-order logic theorem prover, clause preprocessing is an essential step, and the rule of clause elimination is an extremely important part of preprocessing. The traditional clause elimination method based on pure literal rules has some drawbacks which more than enough clauses should be deleted in theory, while less clauses were deleted during implementation. In order to make the clause elimination more accurate, the clauses were classified based on pure literal rules. The first category was called the invalid clause which was not able to form complementary pair to any clause in the clause set through equivalence substitution, and should be completely deleted. The second category was called the relatively invalid clause, which was not complementary to any clause in the current clause set, but could be replaced by other clause after equivalence substitution and should be deleted after certain deduction steps. The clause elimination should actually be a dynamic process where the current clause elimination would affect the invalidity of the determined clauses. Therefore, a clause elimination recursive traversal algorithm for determining clause invalidity was presented and implemented to the prover CSE1.5 (Contradiction Separation Extension 1.5). The problems in first-order logic problem group of the CADE (Conference on Automated DEduction) Automated Theorem Proving (ATP) system competition from 2019 to 2022 were used as the test problems. The CSE1.5_IC with the invalid clause elimination algorithm proved 27 more problems than original CSE1.5 in 300 s. Among all the FNE (FOF theorems without Equality) test cases jointly proved by the two versions of the prover, CSE1.5_IC eliminated 28 more invalid clauses per problem on average than CSE1.5, and the average solution time was reduced by 7.07 s. The experimental results show that the proposed invalid clause elimination algorithm is an effective preprocessing method, which increases the reduction accuracy in the first-order logical clause set, and improves the proving ability and shortens the proof time of automatic theorem prover.

Table and Figures | Reference | Related Articles | Metrics